; COMMAND-LINE: --ho-elim
(set-logic HO_ALL)
(set-info :status unsat)
(declare-sort $$unsorted 0)
(declare-sort tptp.term 0)
(declare-sort tptp.subst 0)
(declare-fun tptp.one () tptp.term)
(declare-fun tptp.ap (tptp.term tptp.term) tptp.term)
(declare-fun tptp.lam (tptp.term) tptp.term)
(declare-fun tptp.sub (tptp.term tptp.subst) tptp.term)
(declare-fun tptp.id () tptp.subst)
(declare-fun tptp.sh () tptp.subst)
(declare-fun tptp.push (tptp.term tptp.subst) tptp.subst)
(declare-fun tptp.comp (tptp.subst tptp.subst) tptp.subst)
(declare-fun tptp.var (tptp.term) Bool)
(declare-fun tptp.pushprop_lem1v2 () Bool)
(declare-fun tptp.pushprop_lem1_gthm () Bool)
(declare-fun tptp.axmap () Bool)
(declare-fun tptp.pushprop_lem0_gthm () Bool)
(declare-fun tptp.shinj () Bool)
(declare-fun tptp.hoasinduction_lem1v2 () Bool)
(declare-fun tptp.hoasinduction_lem1v2_gthm () Bool)
(declare-fun tptp.hoasap (tptp.subst tptp.term tptp.subst tptp.term) tptp.term)
(declare-fun tptp.induction2lem () Bool)
(declare-fun tptp.hoasinduction_lem3v2_f () Bool)
(declare-fun tptp.axvarshift () Bool)
(declare-fun tptp.hoasapinj2 () Bool)
(declare-fun tptp.hoasapnotvar_gthm () Bool)
(declare-fun tptp.hoasapinj1 () Bool)
(declare-fun tptp.ulamvar1 () Bool)
(declare-fun tptp.induction2lem_lthm () Bool)
(declare-fun tptp.hoasinduction_lem3v2_gthm () Bool)
(declare-fun tptp.apnotvar () Bool)
(declare-fun tptp.pushprop_lthm_orig () Bool)
(declare-fun tptp.hoasinduction_lem3v2_f_lthm () Bool)
(declare-fun tptp.hoasinduction_lthm () Bool)
(declare-fun tptp.hoasinduction_no_psi_cond_lthm () Bool)
(declare-fun tptp.hoaslaminj () Bool)
(declare-fun tptp.hoasinduction_lem3aaa () Bool)
(declare-fun tptp.induction2lem_gthm () Bool)
(declare-fun tptp.hoasinduction_lem3aa_lthm () Bool)
(declare-fun tptp.hoasinduction_lem3 () Bool)
(declare-fun tptp.hoasinduction_lem2 () Bool)
(declare-fun tptp.termmset_lthm () Bool)
(declare-fun tptp.hoasinduction_lem1 () Bool)
(declare-fun tptp.hoaslamnotap_lthm () Bool)
(declare-fun tptp.pushprop_lem1v2_lthm () Bool)
(declare-fun tptp.hoasapnotvar () Bool)
(declare-fun tptp.hoasinduction_lem0 () Bool)
(declare-fun tptp.hoasinduction () Bool)
(declare-fun tptp.hoasinduction_gthm () Bool)
(declare-fun tptp.axapp () Bool)
(declare-fun tptp.hoaslamnotvar_lthm () Bool)
(declare-fun tptp.pushprop_lem3v2_lthm () Bool)
(declare-fun tptp.hoasinduction_lem3b_lthm () Bool)
(declare-fun tptp.ulamvarind () Bool)
(declare-fun tptp.induction () Bool)
(declare-fun tptp.hoasinduction_lem3a_lthm () Bool)
(declare-fun tptp.termmset_gthm () Bool)
(declare-fun tptp.hoasinduction_lem3aa () Bool)
(declare-fun tptp.pushprop_lem1v2_gthm () Bool)
(declare-fun tptp.hoaslamnotap_gthm () Bool)
(declare-fun tptp.hoaslamnotvar_gthm () Bool)
(declare-fun tptp.hoasinduction_lem3b_gthm () Bool)
(declare-fun tptp.pushprop_lem2v2 () Bool)
(declare-fun tptp.hoasinduction_lem3a_gthm () Bool)
(declare-fun tptp.axclos () Bool)
(declare-fun tptp.axassoc () Bool)
(declare-fun tptp.hoasinduction_lem2v2 () Bool)
(declare-fun tptp.pushprop_lthm () Bool)
(declare-fun tptp.apinj2 () Bool)
(declare-fun tptp.apinj1 () Bool)
(declare-fun tptp.hoasapinj2_lthm () Bool)
(declare-fun tptp.hoasinduction_lem3v2a () Bool)
(declare-fun tptp.hoasapinj1_lthm () Bool)
(declare-fun tptp.hoaslaminj_lthm () Bool)
(declare-fun tptp.axvarcons () Bool)
(declare-fun tptp.hoaslam (tptp.subst (-> tptp.subst tptp.term tptp.term)) tptp.term)
(declare-fun tptp.axscons () Bool)
(declare-fun tptp.hoasinduction_lem2v2_gthm () Bool)
(declare-fun tptp.axidr () Bool)
(declare-fun tptp.pushprop_lem1 () Bool)
(declare-fun tptp.laminj () Bool)
(declare-fun tptp.hoasinduction_lem3_lthm () Bool)
(declare-fun tptp.pushprop_lem0 () Bool)
(declare-fun tptp.pushprop_gthm () Bool)
(declare-fun tptp.axabs () Bool)
(declare-fun tptp.hoasinduction_lem3v2a_lthm () Bool)
(declare-fun tptp.hoasinduction_lem2_lthm () Bool)
(declare-fun tptp.hoasapinj2_gthm () Bool)
(declare-fun tptp.hoasinduction_p_and_p_prime ((-> tptp.subst tptp.term tptp.subst Bool) (-> tptp.term Bool)) Bool)
(declare-fun tptp.hoasinduction_lem1_lthm () Bool)
(declare-fun tptp.lamnotap () Bool)
(declare-fun tptp.hoasapinj1_gthm () Bool)
(declare-fun tptp.hoaslamnotvar () Bool)
(declare-fun tptp.axidl () Bool)
(declare-fun tptp.hoaslaminj_gthm () Bool)
(declare-fun tptp.induction2_lthm () Bool)
(declare-fun tptp.hoasinduction_lem0_lthm () Bool)
(declare-fun tptp.substmonoid_lthm () Bool)
(declare-fun tptp.pushprop () Bool)
(declare-fun tptp.hoasinduction_lem3_gthm () Bool)
(declare-fun tptp.hoasinduction_lem2_gthm () Bool)
(declare-fun tptp.hoasinduction_lem3b () Bool)
(declare-fun tptp.substmonoid () Bool)
(declare-fun tptp.lamnotvar () Bool)
(declare-fun tptp.hoasinduction_lem3a () Bool)
(declare-fun tptp.hoasinduction_lem1_gthm () Bool)
(declare-fun tptp.hoasinduction_no_psi_cond () Bool)
(declare-fun tptp.induction2_gthm () Bool)
(declare-fun tptp.pushprop_lem2v2_lthm () Bool)
(declare-fun tptp.hoasvar (tptp.subst tptp.term tptp.subst) Bool)
(declare-fun tptp.hoaslamnotap () Bool)
(declare-fun tptp.substmonoid_gthm () Bool)
(declare-fun tptp.ulamvarsh () Bool)
(declare-fun tptp.induction2 () Bool)
(declare-fun tptp.pushprop_lem3v2 () Bool)
(declare-fun tptp.pushprop_lem2v2_gthm () Bool)
(declare-fun tptp.pushprop_lem1_lthm () Bool)
(declare-fun tptp.hoasinduction_lem3v2 () Bool)
(declare-fun tptp.axshiftcons () Bool)
(declare-fun tptp.termmset () Bool)
(declare-fun tptp.pushprop_lem0_lthm () Bool)
(declare-fun tptp.hoasapnotvar_lthm () Bool)
(declare-fun tptp.hoasinduction_lem3v2_lthm () Bool)
(declare-fun tptp.pushprop_p_and_p_prime (tptp.term tptp.subst (-> tptp.term Bool) (-> tptp.term Bool)) Bool)
(declare-fun tptp.axvarid () Bool)
(declare-fun tptp.hoasinduction_lthm_3 () Bool)
(assert (= tptp.axapp (forall ((A tptp.term) (B tptp.term) (M tptp.subst)) (= (@ (@ tptp.sub (@ (@ tptp.ap A) B)) M) (@ (@ tptp.ap (@ (@ tptp.sub A) M)) (@ (@ tptp.sub B) M))))))
(assert (= tptp.axvarcons (forall ((A tptp.term) (M tptp.subst)) (= (@ (@ tptp.sub tptp.one) (@ (@ tptp.push A) M)) A))))
(assert (= tptp.axvarid (forall ((A tptp.term)) (= (@ (@ tptp.sub A) tptp.id) A))))
(assert (= tptp.axabs (forall ((A tptp.term) (M tptp.subst)) (= (@ (@ tptp.sub (@ tptp.lam A)) M) (@ tptp.lam (@ (@ tptp.sub A) (@ (@ tptp.push tptp.one) (@ (@ tptp.comp M) tptp.sh))))))))
(assert (= tptp.axclos (forall ((A tptp.term) (M tptp.subst) (N tptp.subst)) (let ((_let_1 (@ tptp.sub A))) (= (@ (@ tptp.sub (@ _let_1 M)) N) (@ _let_1 (@ (@ tptp.comp M) N)))))))
(assert (= tptp.axidl (forall ((M tptp.subst)) (= (@ (@ tptp.comp tptp.id) M) M))))
(assert (= tptp.axshiftcons (forall ((A tptp.term) (M tptp.subst)) (= (@ (@ tptp.comp tptp.sh) (@ (@ tptp.push A) M)) M))))
(assert (= tptp.axassoc (forall ((M tptp.subst) (N tptp.subst) (K tptp.subst)) (let ((_let_1 (@ tptp.comp M))) (= (@ (@ tptp.comp (@ _let_1 N)) K) (@ _let_1 (@ (@ tptp.comp N) K)))))))
(assert (= tptp.axmap (forall ((A tptp.term) (M tptp.subst) (N tptp.subst)) (= (@ (@ tptp.comp (@ (@ tptp.push A) M)) N) (@ (@ tptp.push (@ (@ tptp.sub A) N)) (@ (@ tptp.comp M) N))))))
(assert (= tptp.axidr (forall ((M tptp.subst)) (= (@ (@ tptp.comp M) tptp.id) M))))
(assert (= tptp.axvarshift (= (@ (@ tptp.push tptp.one) tptp.sh) tptp.id)))
(assert (= tptp.axscons (forall ((M tptp.subst)) (= (@ (@ tptp.push (@ (@ tptp.sub tptp.one) M)) (@ (@ tptp.comp tptp.sh) M)) M))))
(assert (= tptp.ulamvar1 (@ tptp.var tptp.one)))
(assert (= tptp.ulamvarsh (forall ((A tptp.term)) (=> (@ tptp.var A) (@ tptp.var (@ (@ tptp.sub A) tptp.sh))))))
(assert (= tptp.ulamvarind (forall ((P (-> tptp.term Bool))) (=> (@ P tptp.one) (=> (forall ((A tptp.term)) (=> (@ tptp.var A) (=> (@ P A) (@ P (@ (@ tptp.sub A) tptp.sh))))) (forall ((A tptp.term)) (=> (@ tptp.var A) (@ P A))))))))
(assert (= tptp.apinj1 (forall ((A tptp.term) (B tptp.term) (C tptp.term) (D tptp.term)) (=> (= (@ (@ tptp.ap A) C) (@ (@ tptp.ap B) D)) (= A B)))))
(assert (= tptp.apinj2 (forall ((A tptp.term) (B tptp.term) (C tptp.term) (D tptp.term)) (=> (= (@ (@ tptp.ap A) C) (@ (@ tptp.ap B) D)) (= C D)))))
(assert (= tptp.laminj (forall ((A tptp.term) (B tptp.term)) (=> (= (@ tptp.lam A) (@ tptp.lam B)) (= A B)))))
(assert (= tptp.shinj (forall ((A tptp.term) (B tptp.term)) (=> (= (@ (@ tptp.sub A) tptp.sh) (@ (@ tptp.sub B) tptp.sh)) (= A B)))))
(assert (= tptp.lamnotap (forall ((A tptp.term) (B tptp.term) (C tptp.term)) (not (= (@ tptp.lam A) (@ (@ tptp.ap B) C))))))
(assert (= tptp.apnotvar (forall ((A tptp.term) (B tptp.term)) (not (@ tptp.var (@ (@ tptp.ap A) B))))))
(assert (= tptp.lamnotvar (forall ((A tptp.term)) (not (@ tptp.var (@ tptp.lam A))))))
(assert (= tptp.induction (forall ((P (-> tptp.term Bool))) (=> (forall ((A tptp.term)) (=> (@ tptp.var A) (@ P A))) (=> (forall ((A tptp.term) (B tptp.term)) (=> (@ P A) (=> (@ P B) (@ P (@ (@ tptp.ap A) B))))) (=> (forall ((A tptp.term)) (=> (@ P A) (@ P (@ tptp.lam A)))) (forall ((A tptp.term)) (@ P A))))))))
(assert (= tptp.pushprop_p_and_p_prime (lambda ((A tptp.term) (M tptp.subst) (P (-> tptp.term Bool)) (Q (-> tptp.term Bool))) (forall ((X tptp.term)) (= (@ Q X) (@ P (@ (@ tptp.sub X) (@ (@ tptp.push A) M))))))))
(assert (= tptp.pushprop_lem0 (forall ((P (-> tptp.term Bool)) (A tptp.term) (M tptp.subst)) (exists ((Q (-> tptp.term Bool))) (@ (@ (@ (@ tptp.pushprop_p_and_p_prime A) M) P) Q)))))
(assert (= tptp.pushprop_lem0_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction tptp.pushprop_lem0)))))))))))))))))))))))))
(assert (= tptp.pushprop_lem0_lthm tptp.pushprop_lem0))
(assert (= tptp.pushprop_lem1 (forall ((P (-> tptp.term Bool)) (K (-> tptp.term Bool)) (A tptp.term) (M tptp.subst) (B tptp.term)) (=> (@ P A) (@ K (@ (@ tptp.sub A) (@ (@ tptp.push B) M)))))))
(assert (= tptp.pushprop_lem1_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction tptp.pushprop_lem1)))))))))))))))))))))))))
(assert (= tptp.pushprop_lem1_lthm (=> tptp.axvarcons (=> tptp.axclos (=> tptp.axshiftcons (=> tptp.ulamvarind tptp.pushprop_lem1))))))
(assert (= tptp.pushprop_lem1v2 (forall ((P (-> tptp.term Bool)) (Q (-> tptp.term Bool)) (A tptp.term) (M tptp.subst)) (=> (@ P A) (=> (@ (@ (@ (@ tptp.pushprop_p_and_p_prime A) M) P) Q) (@ Q tptp.one))))))
(assert (= tptp.pushprop_lem1v2_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction tptp.pushprop_lem1v2)))))))))))))))))))))))))
(assert (= tptp.pushprop_lem1v2_lthm (=> tptp.axvarcons tptp.pushprop_lem1v2)))
(assert (= tptp.pushprop_lem2v2 (forall ((P (-> tptp.term Bool)) (Q (-> tptp.term Bool)) (A tptp.term) (M tptp.subst)) (=> (@ (@ (@ (@ tptp.pushprop_p_and_p_prime A) M) P) Q) (=> (forall ((B tptp.term)) (=> (@ tptp.var B) (@ P (@ (@ tptp.sub B) M)))) (forall ((C tptp.term)) (=> (@ tptp.var C) (=> (@ Q C) (@ Q (@ (@ tptp.sub C) tptp.sh))))))))))
(assert (= tptp.pushprop_lem2v2_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction tptp.pushprop_lem2v2)))))))))))))))))))))))))
(assert (= tptp.pushprop_lem2v2_lthm (=> tptp.axclos (=> tptp.axshiftcons tptp.pushprop_lem2v2))))
(assert (= tptp.pushprop_lem3v2 (forall ((P (-> tptp.term Bool)) (Q (-> tptp.term Bool)) (A tptp.term) (M tptp.subst)) (=> (@ (@ (@ (@ tptp.pushprop_p_and_p_prime A) M) P) Q) (=> (forall ((B tptp.term)) (=> (@ tptp.var B) (@ Q B))) (forall ((B tptp.term)) (=> (@ tptp.var B) (@ P (@ (@ tptp.sub B) (@ (@ tptp.push A) M))))))))))
(assert (= tptp.pushprop_lem3v2_lthm tptp.pushprop_lem3v2))
(assert (= tptp.pushprop (forall ((P (-> tptp.term Bool)) (A tptp.term) (M tptp.subst)) (=> (forall ((B tptp.term)) (=> (@ tptp.var B) (@ P (@ (@ tptp.sub B) M)))) (=> (@ P A) (forall ((B tptp.term)) (=> (@ tptp.var B) (@ P (@ (@ tptp.sub B) (@ (@ tptp.push A) M))))))))))
(assert (= tptp.pushprop_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction tptp.pushprop)))))))))))))))))))))))))
(assert (= tptp.pushprop_lthm_orig (=> tptp.ulamvar1 (=> tptp.axvarcons (=> tptp.axclos (=> tptp.axshiftcons (=> tptp.ulamvarind tptp.pushprop)))))))
(assert (= tptp.pushprop_lthm (=> tptp.pushprop_lem0 (=> tptp.ulamvar1 (=> tptp.axvarcons (=> tptp.axclos (=> tptp.axshiftcons (=> tptp.ulamvarind tptp.pushprop))))))))
(assert (= tptp.induction2lem (forall ((P (-> tptp.term Bool))) (=> (forall ((A tptp.term) (B tptp.term)) (=> (@ P A) (=> (@ P B) (@ P (@ (@ tptp.ap A) B))))) (=> (forall ((A tptp.term)) (=> (forall ((B tptp.term)) (=> (@ P B) (@ P (@ (@ tptp.sub A) (@ (@ tptp.push B) tptp.id))))) (@ P (@ tptp.lam A)))) (forall ((A tptp.term) (M tptp.subst)) (=> (forall ((B tptp.term)) (=> (@ tptp.var B) (@ P (@ (@ tptp.sub B) M)))) (@ P (@ (@ tptp.sub A) M)))))))))
(assert (= tptp.induction2lem_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop tptp.induction2lem))))))))))))))))))))))))))
(assert (= tptp.induction2lem_lthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axabs (=> tptp.axclos (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.induction (=> tptp.pushprop tptp.induction2lem))))))))))))
(assert (= tptp.induction2 (forall ((P (-> tptp.term Bool))) (=> (forall ((A tptp.term)) (=> (@ tptp.var A) (@ P A))) (=> (forall ((A tptp.term) (B tptp.term)) (=> (@ P A) (=> (@ P B) (@ P (@ (@ tptp.ap A) B))))) (=> (forall ((A tptp.term)) (=> (forall ((B tptp.term)) (=> (@ P B) (@ P (@ (@ tptp.sub A) (@ (@ tptp.push B) tptp.id))))) (@ P (@ tptp.lam A)))) (forall ((A tptp.term)) (@ P A))))))))
(assert (= tptp.induction2_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem tptp.induction2)))))))))))))))))))))))))))
(assert (= tptp.induction2_lthm (=> tptp.axvarid (=> tptp.induction2lem tptp.induction2))))
(assert (= tptp.substmonoid (and (forall ((M tptp.subst) (N tptp.subst) (K tptp.subst)) (let ((_let_1 (@ tptp.comp M))) (= (@ (@ tptp.comp (@ _let_1 N)) K) (@ _let_1 (@ (@ tptp.comp N) K))))) (forall ((M tptp.subst)) (= (@ (@ tptp.comp tptp.id) M) M)) (forall ((M tptp.subst)) (= (@ (@ tptp.comp M) tptp.id) M)))))
(assert (= tptp.substmonoid_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem (=> tptp.induction2 tptp.substmonoid))))))))))))))))))))))))))))
(assert (= tptp.substmonoid_lthm (=> tptp.axidl (=> tptp.axassoc (=> tptp.axidr tptp.substmonoid)))))
(assert (= tptp.termmset (and (forall ((A tptp.term) (M tptp.subst) (N tptp.subst)) (let ((_let_1 (@ tptp.sub A))) (= (@ (@ tptp.sub (@ _let_1 M)) N) (@ _let_1 (@ (@ tptp.comp M) N))))) (forall ((A tptp.term)) (= (@ (@ tptp.sub A) tptp.id) A)))))
(assert (= tptp.termmset_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem (=> tptp.induction2 (=> tptp.substmonoid tptp.termmset)))))))))))))))))))))))))))))
(assert (= tptp.termmset_lthm (=> tptp.axvarid (=> tptp.axclos tptp.termmset))))
(assert (= tptp.hoasap (lambda ((M tptp.subst) (A tptp.term) (N tptp.subst) (B tptp.term)) (@ (@ tptp.ap (@ (@ tptp.sub A) N)) B))))
(assert (= tptp.hoaslam (lambda ((M tptp.subst) (F (-> tptp.subst tptp.term tptp.term))) (@ tptp.lam (@ (@ F tptp.sh) tptp.one)))))
(assert (= tptp.hoasvar (lambda ((M tptp.subst) (A tptp.term) (N tptp.subst)) (@ tptp.var (@ (@ tptp.sub A) N)))))
(assert (= tptp.hoasapinj1 (forall ((A tptp.term) (B tptp.term) (C tptp.term) (D tptp.term)) (let ((_let_1 (@ tptp.hoasap tptp.id))) (=> (= (@ (@ (@ _let_1 A) tptp.id) C) (@ (@ (@ _let_1 B) tptp.id) D)) (= A B))))))
(assert (= tptp.hoasapinj1_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem (=> tptp.induction2 (=> tptp.substmonoid (=> tptp.termmset tptp.hoasapinj1))))))))))))))))))))))))))))))
(assert (= tptp.hoasapinj1_lthm (=> tptp.axvarid (=> tptp.apinj1 tptp.hoasapinj1))))
(assert (= tptp.hoasapinj2 (forall ((A tptp.term) (B tptp.term) (C tptp.term) (D tptp.term)) (let ((_let_1 (@ tptp.hoasap tptp.id))) (=> (= (@ (@ (@ _let_1 A) tptp.id) C) (@ (@ (@ _let_1 B) tptp.id) D)) (= C D))))))
(assert (= tptp.hoasapinj2_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem (=> tptp.induction2 (=> tptp.substmonoid (=> tptp.termmset (=> tptp.hoasapinj1 tptp.hoasapinj2)))))))))))))))))))))))))))))))
(assert (= tptp.hoasapinj2_lthm (=> tptp.apinj2 tptp.hoasapinj2)))
(assert (= tptp.hoaslaminj (forall ((F (-> tptp.subst tptp.term tptp.term))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (@ (@ tptp.sub (@ (@ F M) A)) N) (@ (@ F (@ (@ tptp.comp M) N)) (@ (@ tptp.sub A) N)))) (forall ((G (-> tptp.subst tptp.term tptp.term))) (let ((_let_1 (@ tptp.hoaslam tptp.id))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (@ (@ tptp.sub (@ (@ G M) A)) N) (@ (@ G (@ (@ tptp.comp M) N)) (@ (@ tptp.sub A) N)))) (=> (= (@ _let_1 (lambda ((M tptp.subst) (A tptp.term)) (@ (@ F M) A))) (@ _let_1 (lambda ((M tptp.subst) (A tptp.term)) (@ (@ G M) A)))) (forall ((M tptp.subst) (A tptp.term)) (= (@ (@ F M) A) (@ (@ G M) A)))))))))))
(assert (= tptp.hoaslaminj_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem (=> tptp.induction2 (=> tptp.substmonoid (=> tptp.termmset (=> tptp.hoasapinj1 (=> tptp.hoasapinj2 tptp.hoaslaminj))))))))))))))))))))))))))))))))
(assert (= tptp.hoaslaminj_lthm (=> tptp.axvarcons (=> tptp.axshiftcons (=> tptp.laminj tptp.hoaslaminj)))))
(assert (= tptp.hoaslamnotap (forall ((F (-> tptp.subst tptp.term tptp.term))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (@ (@ tptp.sub (@ (@ F M) A)) N) (@ (@ F (@ (@ tptp.comp M) N)) (@ (@ tptp.sub A) N)))) (forall ((A tptp.term) (B tptp.term)) (not (= (@ (@ tptp.hoaslam tptp.id) (lambda ((M tptp.subst) (C tptp.term)) (@ (@ F M) C))) (@ (@ (@ (@ tptp.hoasap tptp.id) A) tptp.id) B))))))))
(assert (= tptp.hoaslamnotap_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem (=> tptp.induction2 (=> tptp.substmonoid (=> tptp.termmset (=> tptp.hoasapinj1 (=> tptp.hoasapinj2 (=> tptp.hoaslaminj tptp.hoaslamnotap)))))))))))))))))))))))))))))))))
(assert (= tptp.hoaslamnotap_lthm (=> tptp.lamnotap tptp.hoaslamnotap)))
(assert (= tptp.hoaslamnotvar (forall ((F (-> tptp.subst tptp.term tptp.term))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (@ (@ tptp.sub (@ (@ F M) A)) N) (@ (@ F (@ (@ tptp.comp M) N)) (@ (@ tptp.sub A) N)))) (not (@ (@ (@ tptp.hoasvar tptp.id) (@ (@ tptp.hoaslam tptp.id) (lambda ((M tptp.subst) (A tptp.term)) (@ (@ F M) A)))) tptp.id))))))
(assert (= tptp.hoaslamnotvar_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem (=> tptp.induction2 (=> tptp.substmonoid (=> tptp.termmset (=> tptp.hoasapinj1 (=> tptp.hoasapinj2 (=> tptp.hoaslaminj (=> tptp.hoaslamnotap tptp.hoaslamnotvar))))))))))))))))))))))))))))))))))
(assert (= tptp.hoaslamnotvar_lthm (=> tptp.axvarid (=> tptp.lamnotvar tptp.hoaslamnotvar))))
(assert (= tptp.hoasapnotvar (forall ((A tptp.term) (B tptp.term)) (not (@ (@ (@ tptp.hoasvar tptp.id) (@ (@ (@ (@ tptp.hoasap tptp.id) A) tptp.id) B)) tptp.id)))))
(assert (= tptp.hoasapnotvar_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem (=> tptp.induction2 (=> tptp.substmonoid (=> tptp.termmset (=> tptp.hoasapinj1 (=> tptp.hoasapinj2 (=> tptp.hoaslaminj (=> tptp.hoaslamnotap (=> tptp.hoaslamnotvar tptp.hoasapnotvar)))))))))))))))))))))))))))))))))))
(assert (= tptp.hoasapnotvar_lthm (=> tptp.axvarid (=> tptp.apnotvar tptp.hoasapnotvar))))
(assert (= tptp.hoasinduction_p_and_p_prime (lambda ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool))) (forall ((X tptp.term)) (= (@ Q X) (@ (@ (@ P tptp.id) X) tptp.id))))))
(assert (= tptp.hoasinduction_lem0 (forall ((P (-> tptp.subst tptp.term tptp.subst Bool))) (exists ((Q (-> tptp.term Bool))) (@ (@ tptp.hoasinduction_p_and_p_prime P) Q)))))
(assert (= tptp.hoasinduction_lem0_lthm tptp.hoasinduction_lem0))
(assert (= tptp.hoasinduction_lem1v2 (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (=> (@ (@ (@ P M) A) (@ (@ tptp.comp K) N)) (@ (@ (@ P (@ (@ tptp.comp M) K)) (@ (@ tptp.sub A) K)) N))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (=> (@ (@ (@ P (@ (@ tptp.comp M) K)) (@ (@ tptp.sub A) K)) N) (@ (@ (@ P M) A) (@ (@ tptp.comp K) N)))) (=> (forall ((A tptp.term)) (=> (@ (@ (@ tptp.hoasvar tptp.id) A) tptp.id) (@ (@ (@ P tptp.id) A) tptp.id))) (=> (@ (@ tptp.hoasinduction_p_and_p_prime P) Q) (forall ((A tptp.term)) (=> (@ tptp.var A) (@ Q A))))))))))
(assert (= tptp.hoasinduction_lem1v2_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem (=> tptp.induction2 (=> tptp.substmonoid (=> tptp.termmset (=> tptp.hoasapinj1 (=> tptp.hoasapinj2 (=> tptp.hoaslaminj (=> tptp.hoaslamnotap (=> tptp.hoaslamnotvar (=> tptp.hoasapnotvar tptp.hoasinduction_lem1v2))))))))))))))))))))))))))))))))))))
(assert (= tptp.hoasinduction_lem2v2 (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (=> (@ (@ (@ P M) A) (@ (@ tptp.comp K) N)) (@ (@ (@ P (@ (@ tptp.comp M) K)) (@ (@ tptp.sub A) K)) N))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (=> (@ (@ (@ P (@ (@ tptp.comp M) K)) (@ (@ tptp.sub A) K)) N) (@ (@ (@ P M) A) (@ (@ tptp.comp K) N)))) (=> (forall ((A tptp.term) (B tptp.term)) (let ((_let_1 (@ P tptp.id))) (=> (@ (@ _let_1 A) tptp.id) (=> (@ (@ _let_1 B) tptp.id) (@ (@ _let_1 (@ (@ (@ (@ tptp.hoasap tptp.id) A) tptp.id) B)) tptp.id))))) (=> (@ (@ tptp.hoasinduction_p_and_p_prime P) Q) (forall ((A tptp.term) (B tptp.term)) (=> (@ Q A) (=> (@ Q B) (@ Q (@ (@ tptp.ap A) B))))))))))))
(assert (= tptp.hoasinduction_lem2v2_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem (=> tptp.induction2 (=> tptp.substmonoid (=> tptp.termmset (=> tptp.hoasapinj1 (=> tptp.hoasapinj2 (=> tptp.hoaslaminj (=> tptp.hoaslamnotap (=> tptp.hoaslamnotvar (=> tptp.hoasapnotvar tptp.hoasinduction_lem2v2))))))))))))))))))))))))))))))))))))
(assert (= tptp.hoasinduction_lem3v2_f (forall ((B tptp.term)) (exists ((F (-> tptp.subst tptp.term tptp.term))) (forall ((A tptp.term) (M tptp.subst)) (= (@ (@ F M) A) (@ (@ tptp.sub B) (@ (@ tptp.push A) M))))))))
(assert (= tptp.hoasinduction_lem3v2_f_lthm tptp.hoasinduction_lem3v2_f))
(assert (= tptp.hoasinduction_lem3v2 (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (=> (@ (@ (@ P M) A) (@ (@ tptp.comp K) N)) (@ (@ (@ P (@ (@ tptp.comp M) K)) (@ (@ tptp.sub A) K)) N))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (=> (@ (@ (@ P (@ (@ tptp.comp M) K)) (@ (@ tptp.sub A) K)) N) (@ (@ (@ P M) A) (@ (@ tptp.comp K) N)))) (=> (forall ((F (-> tptp.subst tptp.term tptp.term))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (@ (@ tptp.sub (@ (@ F M) A)) N) (@ (@ F (@ (@ tptp.comp M) N)) (@ (@ tptp.sub A) N)))) (=> (forall ((A tptp.term)) (let ((_let_1 (@ P tptp.id))) (=> (@ (@ _let_1 A) tptp.id) (@ (@ _let_1 (@ (@ F tptp.id) A)) tptp.id)))) (@ (@ (@ P tptp.id) (@ (@ tptp.hoaslam tptp.id) (lambda ((M tptp.subst) (A tptp.term)) (@ (@ F M) A)))) tptp.id)))) (=> (@ (@ tptp.hoasinduction_p_and_p_prime P) Q) (forall ((A tptp.term)) (=> (forall ((B tptp.term)) (=> (@ Q B) (@ Q (@ (@ tptp.sub A) (@ (@ tptp.push B) tptp.id))))) (@ Q (@ tptp.lam A)))))))))))
(assert (= tptp.hoasinduction_lem3v2_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem (=> tptp.induction2 (=> tptp.substmonoid (=> tptp.termmset (=> tptp.hoasapinj1 (=> tptp.hoasapinj2 (=> tptp.hoaslaminj (=> tptp.hoaslamnotap (=> tptp.hoaslamnotvar (=> tptp.hoasapnotvar tptp.hoasinduction_lem3v2))))))))))))))))))))))))))))))))))))
(assert (= tptp.hoasinduction_lem3v2_lthm (=> tptp.axvarid (=> tptp.axvarshift (=> tptp.axclos (=> tptp.axmap tptp.hoasinduction_lem3v2))))))
(assert (= tptp.hoasinduction_lem3v2a (forall ((P (-> tptp.subst tptp.term tptp.subst Bool)) (Q (-> tptp.term Bool))) (=> (forall ((F (-> tptp.subst tptp.term tptp.term))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (@ (@ tptp.sub (@ (@ F M) A)) N) (@ (@ F (@ (@ tptp.comp M) N)) (@ (@ tptp.sub A) N)))) (=> (forall ((A tptp.term)) (let ((_let_1 (@ P tptp.id))) (=> (@ (@ _let_1 A) tptp.id) (@ (@ _let_1 (@ (@ F tptp.id) A)) tptp.id)))) (@ (@ (@ P tptp.id) (@ (@ tptp.hoaslam tptp.id) (lambda ((M tptp.subst) (A tptp.term)) (@ (@ F M) A)))) tptp.id)))) (=> (@ (@ tptp.hoasinduction_p_and_p_prime P) Q) (forall ((A tptp.term)) (=> (forall ((B tptp.term)) (=> (@ Q B) (@ Q (@ (@ tptp.sub A) (@ (@ tptp.push B) tptp.id))))) (@ Q (@ tptp.lam A)))))))))
(assert (= tptp.hoasinduction_lem3v2a_lthm (=> tptp.hoasinduction_lem3v2_f (=> tptp.axvarid (=> tptp.axvarshift (=> tptp.axclos (=> tptp.axmap tptp.hoasinduction_lem3v2a)))))))
(assert (= tptp.hoasinduction_lem1 (forall ((P (-> tptp.subst tptp.term tptp.subst Bool))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (=> (@ (@ (@ P M) A) (@ (@ tptp.comp K) N)) (@ (@ (@ P (@ (@ tptp.comp M) K)) (@ (@ tptp.sub A) K)) N))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (=> (@ (@ (@ P (@ (@ tptp.comp M) K)) (@ (@ tptp.sub A) K)) N) (@ (@ (@ P M) A) (@ (@ tptp.comp K) N)))) (=> (forall ((A tptp.term)) (=> (@ (@ (@ tptp.hoasvar tptp.id) A) tptp.id) (@ (@ (@ P tptp.id) A) tptp.id))) (forall ((A tptp.term)) (=> (@ tptp.var A) (@ (@ (@ P tptp.id) A) tptp.id)))))))))
(assert (= tptp.hoasinduction_lem1_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem (=> tptp.induction2 (=> tptp.substmonoid (=> tptp.termmset (=> tptp.hoasapinj1 (=> tptp.hoasapinj2 (=> tptp.hoaslaminj (=> tptp.hoaslamnotap (=> tptp.hoaslamnotvar (=> tptp.hoasapnotvar tptp.hoasinduction_lem1))))))))))))))))))))))))))))))))))))
(assert (= tptp.hoasinduction_lem1_lthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem (=> tptp.induction2 (=> tptp.substmonoid (=> tptp.termmset (=> tptp.hoasapinj1 (=> tptp.hoasapinj2 (=> tptp.hoaslaminj (=> tptp.hoaslamnotap (=> tptp.hoaslamnotvar (=> tptp.hoasapnotvar tptp.hoasinduction_lem1))))))))))))))))))))))))))))))))))))
(assert (= tptp.hoasinduction_lem2 (forall ((P (-> tptp.subst tptp.term tptp.subst Bool))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (=> (@ (@ (@ P M) A) (@ (@ tptp.comp K) N)) (@ (@ (@ P (@ (@ tptp.comp M) K)) (@ (@ tptp.sub A) K)) N))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (=> (@ (@ (@ P (@ (@ tptp.comp M) K)) (@ (@ tptp.sub A) K)) N) (@ (@ (@ P M) A) (@ (@ tptp.comp K) N)))) (=> (forall ((A tptp.term) (B tptp.term)) (let ((_let_1 (@ P tptp.id))) (=> (@ (@ _let_1 A) tptp.id) (=> (@ (@ _let_1 B) tptp.id) (@ (@ _let_1 (@ (@ (@ (@ tptp.hoasap tptp.id) A) tptp.id) B)) tptp.id))))) (forall ((A tptp.term) (B tptp.term)) (let ((_let_1 (@ P tptp.id))) (=> (@ (@ _let_1 A) tptp.id) (=> (@ (@ _let_1 B) tptp.id) (@ (@ _let_1 (@ (@ tptp.ap A) B)) tptp.id)))))))))))
(assert (= tptp.hoasinduction_lem2_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem (=> tptp.induction2 (=> tptp.substmonoid (=> tptp.termmset (=> tptp.hoasapinj1 (=> tptp.hoasapinj2 (=> tptp.hoaslaminj (=> tptp.hoaslamnotap (=> tptp.hoaslamnotvar (=> tptp.hoasapnotvar tptp.hoasinduction_lem2))))))))))))))))))))))))))))))))))))
(assert (= tptp.hoasinduction_lem2_lthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem (=> tptp.induction2 (=> tptp.substmonoid (=> tptp.termmset (=> tptp.hoasapinj1 (=> tptp.hoasapinj2 (=> tptp.hoaslaminj (=> tptp.hoaslamnotap (=> tptp.hoaslamnotvar (=> tptp.hoasapnotvar tptp.hoasinduction_lem2))))))))))))))))))))))))))))))))))))
(assert (= tptp.hoasinduction_lem3aa (forall ((P (-> tptp.subst tptp.term tptp.subst Bool))) (=> (forall ((F (-> tptp.subst tptp.term tptp.term))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (@ (@ tptp.sub (@ (@ F M) A)) N) (@ (@ F (@ (@ tptp.comp M) N)) (@ (@ tptp.sub A) N)))) (=> (forall ((A tptp.term)) (let ((_let_1 (@ P tptp.id))) (=> (@ (@ _let_1 A) tptp.id) (@ (@ _let_1 (@ (@ F tptp.id) A)) tptp.id)))) (@ (@ (@ P tptp.id) (@ (@ tptp.hoaslam tptp.id) (lambda ((M tptp.subst) (A tptp.term)) (@ (@ F M) A)))) tptp.id)))) (forall ((A tptp.term)) (=> (forall ((B tptp.term)) (let ((_let_1 (@ P tptp.id))) (=> (@ (@ _let_1 B) tptp.id) (@ (@ _let_1 (@ (@ tptp.sub A) (@ (@ tptp.push B) tptp.id))) tptp.id)))) (@ (@ (@ P tptp.id) (@ tptp.lam (@ (@ tptp.sub A) (@ (@ tptp.push tptp.one) tptp.sh)))) tptp.id)))))))
(assert (= tptp.hoasinduction_lem3aa_lthm (=> tptp.axclos (=> tptp.axmap tptp.hoasinduction_lem3aa))))
(assert (= tptp.hoasinduction_lem3aaa (forall ((P (-> tptp.subst tptp.term tptp.subst Bool))) (=> (forall ((F (-> tptp.subst tptp.term tptp.term))) (=> (exists ((C tptp.term)) (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (let ((_let_1 (@ (@ tptp.sub A) N))) (let ((_let_2 (@ (@ tptp.comp M) N))) (let ((_let_3 (@ tptp.sub C))) (and (= (@ (@ tptp.sub (@ (@ F M) A)) N) (@ (@ tptp.sub (@ _let_3 (@ (@ tptp.push A) M))) N)) (= (@ _let_3 (@ (@ tptp.push _let_1) _let_2)) (@ (@ F _let_2) _let_1)))))))) (=> (forall ((A tptp.term)) (let ((_let_1 (@ P tptp.id))) (=> (@ (@ _let_1 A) tptp.id) (@ (@ _let_1 (@ (@ F tptp.id) A)) tptp.id)))) (@ (@ (@ P tptp.id) (@ (@ tptp.hoaslam tptp.id) (lambda ((M tptp.subst) (A tptp.term)) (@ (@ F M) A)))) tptp.id)))) (forall ((A tptp.term)) (=> (forall ((B tptp.term)) (let ((_let_1 (@ P tptp.id))) (=> (@ (@ _let_1 B) tptp.id) (@ (@ _let_1 (@ (@ tptp.sub A) (@ (@ tptp.push B) tptp.id))) tptp.id)))) (@ (@ (@ P tptp.id) (@ tptp.lam (@ (@ tptp.sub A) (@ (@ tptp.push tptp.one) tptp.sh)))) tptp.id)))))))
(assert (= tptp.hoasinduction_lem3 (forall ((P (-> tptp.subst tptp.term tptp.subst Bool))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (=> (@ (@ (@ P M) A) (@ (@ tptp.comp K) N)) (@ (@ (@ P (@ (@ tptp.comp M) K)) (@ (@ tptp.sub A) K)) N))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (=> (@ (@ (@ P (@ (@ tptp.comp M) K)) (@ (@ tptp.sub A) K)) N) (@ (@ (@ P M) A) (@ (@ tptp.comp K) N)))) (=> (forall ((F (-> tptp.subst tptp.term tptp.term))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (@ (@ tptp.sub (@ (@ F M) A)) N) (@ (@ F (@ (@ tptp.comp M) N)) (@ (@ tptp.sub A) N)))) (=> (forall ((A tptp.term)) (let ((_let_1 (@ P tptp.id))) (=> (@ (@ _let_1 A) tptp.id) (@ (@ _let_1 (@ (@ F tptp.id) A)) tptp.id)))) (@ (@ (@ P tptp.id) (@ (@ tptp.hoaslam tptp.id) (lambda ((M tptp.subst) (A tptp.term)) (@ (@ F M) A)))) tptp.id)))) (forall ((A tptp.term)) (=> (forall ((B tptp.term)) (let ((_let_1 (@ P tptp.id))) (=> (@ (@ _let_1 B) tptp.id) (@ (@ _let_1 (@ (@ tptp.sub A) (@ (@ tptp.push B) tptp.id))) tptp.id)))) (@ (@ (@ P tptp.id) (@ tptp.lam A)) tptp.id)))))))))
(assert (= tptp.hoasinduction_lem3_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem (=> tptp.induction2 (=> tptp.substmonoid (=> tptp.termmset (=> tptp.hoasapinj1 (=> tptp.hoasapinj2 (=> tptp.hoaslaminj (=> tptp.hoaslamnotap (=> tptp.hoaslamnotvar (=> tptp.hoasapnotvar (=> tptp.hoasinduction_lem1 (=> tptp.hoasinduction_lem2 tptp.hoasinduction_lem3))))))))))))))))))))))))))))))))))))))
(assert (= tptp.hoasinduction_lem3_lthm (=> tptp.axvarid (=> tptp.axvarshift (=> tptp.hoasinduction_lem3aa tptp.hoasinduction_lem3)))))
(assert (= tptp.hoasinduction_lem3a (forall ((P (-> tptp.subst tptp.term tptp.subst Bool))) (=> (forall ((F (-> tptp.subst tptp.term tptp.term))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (@ (@ tptp.sub (@ (@ F M) A)) N) (@ (@ F (@ (@ tptp.comp M) N)) (@ (@ tptp.sub A) N)))) (=> (forall ((A tptp.term)) (let ((_let_1 (@ P tptp.id))) (=> (@ (@ _let_1 A) tptp.id) (@ (@ _let_1 (@ (@ F tptp.id) A)) tptp.id)))) (@ (@ (@ P tptp.id) (@ (@ tptp.hoaslam tptp.id) (lambda ((M tptp.subst) (A tptp.term)) (@ (@ F M) A)))) tptp.id)))) (forall ((A tptp.term)) (=> (forall ((B tptp.term)) (let ((_let_1 (@ P tptp.id))) (=> (@ (@ _let_1 B) tptp.id) (@ (@ _let_1 (@ (@ tptp.sub A) (@ (@ tptp.push B) tptp.id))) tptp.id)))) (@ (@ (@ P tptp.id) (@ tptp.lam A)) tptp.id)))))))
(assert (= tptp.hoasinduction_lem3a_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem (=> tptp.induction2 (=> tptp.substmonoid (=> tptp.termmset (=> tptp.hoasapinj1 (=> tptp.hoasapinj2 (=> tptp.hoaslaminj (=> tptp.hoaslamnotap (=> tptp.hoaslamnotvar (=> tptp.hoasapnotvar (=> tptp.hoasinduction_lem1 (=> tptp.hoasinduction_lem2 tptp.hoasinduction_lem3a))))))))))))))))))))))))))))))))))))))
(assert (= tptp.hoasinduction_lem3a_lthm (=> tptp.axvarid (=> tptp.axvarshift (=> tptp.hoasinduction_lem3aa tptp.hoasinduction_lem3a)))))
(assert (= tptp.hoasinduction_lem3b (forall ((B tptp.term)) (exists ((F (-> tptp.subst tptp.term tptp.term))) (= (@ (@ tptp.sub B) (@ (@ tptp.push tptp.one) tptp.sh)) (@ (@ F tptp.sh) tptp.one))))))
(assert (= tptp.hoasinduction_lem3b_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem (=> tptp.induction2 (=> tptp.substmonoid (=> tptp.termmset (=> tptp.hoasapinj1 (=> tptp.hoasapinj2 (=> tptp.hoaslaminj (=> tptp.hoaslamnotap (=> tptp.hoaslamnotvar (=> tptp.hoasapnotvar (=> tptp.hoasinduction_lem1 (=> tptp.hoasinduction_lem2 tptp.hoasinduction_lem3b))))))))))))))))))))))))))))))))))))))
(assert (= tptp.hoasinduction_lem3b_lthm tptp.hoasinduction_lem3b))
(assert (= tptp.hoasinduction (forall ((P (-> tptp.subst tptp.term tptp.subst Bool))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (=> (@ (@ (@ P M) A) (@ (@ tptp.comp K) N)) (@ (@ (@ P (@ (@ tptp.comp M) K)) (@ (@ tptp.sub A) K)) N))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst) (K tptp.subst)) (=> (@ (@ (@ P (@ (@ tptp.comp M) K)) (@ (@ tptp.sub A) K)) N) (@ (@ (@ P M) A) (@ (@ tptp.comp K) N)))) (=> (forall ((A tptp.term)) (=> (@ (@ (@ tptp.hoasvar tptp.id) A) tptp.id) (@ (@ (@ P tptp.id) A) tptp.id))) (=> (forall ((A tptp.term) (B tptp.term)) (let ((_let_1 (@ P tptp.id))) (=> (@ (@ _let_1 A) tptp.id) (=> (@ (@ _let_1 B) tptp.id) (@ (@ _let_1 (@ (@ (@ (@ tptp.hoasap tptp.id) A) tptp.id) B)) tptp.id))))) (=> (forall ((F (-> tptp.subst tptp.term tptp.term))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (@ (@ tptp.sub (@ (@ F M) A)) N) (@ (@ F (@ (@ tptp.comp M) N)) (@ (@ tptp.sub A) N)))) (=> (forall ((A tptp.term)) (let ((_let_1 (@ P tptp.id))) (=> (@ (@ _let_1 A) tptp.id) (@ (@ _let_1 (@ (@ F tptp.id) A)) tptp.id)))) (@ (@ (@ P tptp.id) (@ (@ tptp.hoaslam tptp.id) (lambda ((M tptp.subst) (A tptp.term)) (@ (@ F M) A)))) tptp.id)))) (forall ((A tptp.term)) (@ (@ (@ P tptp.id) A) tptp.id))))))))))
(assert (= tptp.hoasinduction_gthm (=> tptp.axapp (=> tptp.axvarcons (=> tptp.axvarid (=> tptp.axabs (=> tptp.axclos (=> tptp.axidl (=> tptp.axshiftcons (=> tptp.axassoc (=> tptp.axmap (=> tptp.axidr (=> tptp.axvarshift (=> tptp.axscons (=> tptp.ulamvar1 (=> tptp.ulamvarsh (=> tptp.ulamvarind (=> tptp.apinj1 (=> tptp.apinj2 (=> tptp.laminj (=> tptp.shinj (=> tptp.lamnotap (=> tptp.apnotvar (=> tptp.lamnotvar (=> tptp.induction (=> tptp.pushprop (=> tptp.induction2lem (=> tptp.induction2 (=> tptp.substmonoid (=> tptp.termmset (=> tptp.hoasapinj1 (=> tptp.hoasapinj2 (=> tptp.hoaslaminj (=> tptp.hoaslamnotap (=> tptp.hoaslamnotvar (=> tptp.hoasapnotvar (=> tptp.hoasinduction_lem1 (=> tptp.hoasinduction_lem2 (=> tptp.hoasinduction_lem3 tptp.hoasinduction)))))))))))))))))))))))))))))))))))))))
(assert (= tptp.hoasinduction_lthm (=> tptp.induction2 (=> tptp.hoasinduction_lem1 (=> tptp.hoasinduction_lem2 (=> tptp.hoasinduction_lem3 tptp.hoasinduction))))))
(assert (= tptp.hoasinduction_lthm_3 (=> tptp.hoasinduction_lem0 (=> tptp.induction2 (=> tptp.axvarid (=> tptp.hoasinduction_lem3v2a tptp.hoasinduction))))))
(assert (= tptp.hoasinduction_no_psi_cond (forall ((P (-> tptp.subst tptp.term tptp.subst Bool))) (=> (forall ((A tptp.term) (B tptp.term)) (let ((_let_1 (@ P tptp.id))) (=> (@ (@ _let_1 A) tptp.id) (=> (@ (@ _let_1 B) tptp.id) (@ (@ _let_1 (@ (@ (@ (@ tptp.hoasap tptp.id) A) tptp.id) B)) tptp.id))))) (=> (forall ((F (-> tptp.subst tptp.term tptp.term))) (=> (forall ((M tptp.subst) (A tptp.term) (N tptp.subst)) (= (@ (@ tptp.sub (@ (@ F M) A)) N) (@ (@ F (@ (@ tptp.comp M) N)) (@ (@ tptp.sub A) N)))) (=> (forall ((A tptp.term)) (let ((_let_1 (@ P tptp.id))) (=> (@ (@ _let_1 A) tptp.id) (@ (@ _let_1 (@ (@ F tptp.id) A)) tptp.id)))) (@ (@ (@ P tptp.id) (@ (@ tptp.hoaslam tptp.id) (lambda ((M tptp.subst) (A tptp.term)) (@ (@ F M) A)))) tptp.id)))) (forall ((A tptp.term)) (@ (@ (@ P tptp.id) A) tptp.id)))))))
(assert (= tptp.hoasinduction_no_psi_cond_lthm (=> tptp.hoasinduction_lem0 (=> tptp.induction2 (=> tptp.axvarid (=> tptp.hoasinduction_lem3v2a tptp.hoasinduction_no_psi_cond))))))
(assert (not tptp.pushprop_lem1v2_lthm))
(set-info :filename involved_parsing_ALG248^3)
(check-sat-assuming ( true ))
